Inference at * 1 
Iof proof for Lemma sub functionality wrt le:



1. i1 : 
2. i2 : 
3. j1 : 
4. j2 : 
5. i1  j1
6. i2  j2 
  (i1 - i2)  (j1 - j2) 

latex

 by ((ArithSimp 0) 
CollapseTHENA ((Auto_aux (first_nat 1:n) ((first_nat 1:n),(first_nat 3:n
C)) (first_tok :t) inil_term))) 

latex

C1: 

C1:   (i1+(-i2))  (j1+(-j2))
C.

Definitions	t  T, True, T, False, P  Q, A, x:A. B(x), , i  j , A  B
Lemmas	true wf, squash wf, le wf